A, B, C:MsgA. C ||decl A  C ||decl B  A ||decl B  A  B  C = A  B  C  MsgA 

latex

Definitions

f || g, Id, IdDeq, f  g, Knd, f  g, KindDeq, M1 ||decl M2, M1  M2, MsgA, P & Q, mk-ma, T, True, product-deq(A;B;a;b), IdLnkDeq, Valtype(da;k), a:A fp B(a), Prop, locl(a), State(ds), f(x)?z, Top, 1of(t), P  Q, rcv(l,tg), 2of(t), x. t(x), x:A. B(x), IdLnk, t  T

Lemmas

Knd wf, IdLnk wf, pi2 wf, rcv wf, Kind-deq wf, fpf-join wf, subtype-fpf-cap-void, pi1 wf, top wf, subtype-fpf-cap-top, id-deq wf, Id wf, fpf-cap wf, subtype rel list, subtype rel function, subtype rel self, subtype rel dep function, ma-state wf, subtype rel product, subtype-fpf2, fpf-sub-join-left, locl wf, idlnk-deq wf, product-deq wf, fpf-trivial-subtype-top, ma-valtype wf, fpf-join-assoc, fpf wf, true wf, squash wf, mk-ma wf, fpf-compatible-join, fpf-compatible-symmetry, fpf-sub-join-right, fpf-sub transitivity, fpf-compatible wf, msga wf